Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    x - 0  → x
2:    s(x) - s(y)  → x - y
3:    0 + y  → y
4:    s(x) + y  → s(x + y)
5:    x * 0  → 0
6:    x * s(y)  → x + (x * y)
7:    p(s(x))  → x
8:    f(s(x))  → f(p(s(x) * s(x)) - (s(x) * s(x)))
There are 8 dependency pairs:
9:    s(x) -# s(y)  → x -# y
10:    s(x) +# y  → x +# y
11:    x *# s(y)  → x +# (x * y)
12:    x *# s(y)  → x *# y
13:    F(s(x))  → F(p(s(x) * s(x)) - (s(x) * s(x)))
14:    F(s(x))  → p(s(x) * s(x)) -# (s(x) * s(x))
15:    F(s(x))  → P(s(x) * s(x))
16:    F(s(x))  → s(x) *# s(x)
The approximated dependency graph contains 4 SCCs: {10}, {12}, {9} and {13}.
Tyrolean Termination Tool  (0.09 seconds)   ---  May 4, 2006